module Test.Kore.Builtin.InternalBytes (
    test_update,
    test_get,
    test_substr,
    test_replaceAt,
    test_padRight,
    test_padLeft,
    test_reverse,
    test_length,
    test_concat,
    test_reverse_length,
    test_update_get,
    test_bytes2string_string2bytes,
    test_decodeBytes_encodeBytes,
    test_decodeBytes,
    test_encodeBytes,
    test_int2bytes,
    test_bytes2int,
    test_InternalBytes,
    test_unparse,
) where

import Control.Exception (ErrorCall (..), try)
import Data.ByteString (
    ByteString,
 )
import Data.ByteString qualified as ByteString
import Data.ByteString.Char8 qualified as BS
import Data.Char (
    ord,
 )
import Data.Text (
    Text,
 )
import Data.Text qualified as T
import Hedgehog hiding (
    Concrete,
    test,
 )
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Kore.Builtin.Encoding qualified as E
import Kore.Builtin.InternalBytes (decodeBytesKey, encodeBytesKey)
import Kore.Builtin.InternalBytes qualified as InternalBytes
import Kore.Internal.MultiOr qualified as MultiOr
import Kore.Internal.OrPattern (OrPattern)
import Kore.Internal.OrPattern qualified as OrPattern
import Kore.Internal.Pattern
import Kore.Internal.Pattern qualified as Pattern
import Kore.Internal.TermLike
import Kore.Rewrite.RewritingVariable (
    RewritingVariableName,
    mkConfigVariable,
 )
import Kore.Unparser
import Prelude.Kore
import Pretty qualified
import Test.Kore.Builtin.Builtin
import Test.Kore.Builtin.Definition
import Test.Kore.Builtin.Int qualified as Test.Int
import Test.Kore.Builtin.String qualified as Test.String
import Test.SMT
import Test.Tasty
import Test.Tasty.HUnit.Ext

genString :: Gen Text
genString = Gen.text (Range.linear 0 256) Gen.latin1

genString' :: Int -> Gen Text
genString' i = Gen.text (Range.linear 0 i) Gen.latin1

test_update :: [TestTree]
test_update =
    [ testPropertyWithSolver "∀ b v. update b 0 v = v" $ do
        val <- forAll Gen.unicode
        let val' = toInteger $ ord val
            bytes = BS.pack [val]
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    updateBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal 0
                    , Test.Int.asInternal val'
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b i v (i < 0). update b i v = ⊥" $ do
        str <- forAll genString
        val <- forAll Gen.unicode
        idx <- forAll $ Gen.int (Range.linear (-256) (-1))
        let bytes = E.encode8Bit str
            val' = toInteger $ ord val
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    updateBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger idx)
                    , Test.Int.asInternal val'
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b i v (i > length bs). update b i v = ⊥" $ do
        str <- forAll genString
        val <- forAll Gen.unicode
        let bytes = E.encode8Bit str
            val' = toInteger $ ord val
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    updateBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger $ BS.length bytes)
                    , Test.Int.asInternal val'
                    ]
        (===) expect actual
    , testBytes
        "update 'abcd' 0 'x' = 'xbcd'"
        updateBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 0
        , Test.Int.asInternal (toInteger $ ord 'x')
        ]
        (asOrPattern "xbcd")
    , testBytes
        "update 'abcd' 3 'x' = 'abcx"
        updateBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 3
        , Test.Int.asInternal (toInteger $ ord 'x')
        ]
        (asOrPattern "abcx")
    ]

test_get :: [TestTree]
test_get =
    [ testPropertyWithSolver "∀ b i (i < 0). get b i = ⊥" $ do
        str <- forAll genString
        idx <- forAll $ Gen.int (Range.linear (-256) (-1))
        let bytes = E.encode8Bit str
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    getBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger idx)
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b i (i > len b). get b i = ⊥" $ do
        str <- forAll genString
        let bytes = E.encode8Bit str
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    getBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger $ BS.length bytes)
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ i. get empty i = ⊥" $ do
        idx <- forAll $ Gen.int (Range.linear 0 256)
        let expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    getBytesSymbol
                    [ asInternal ""
                    , Test.Int.asInternal (toInteger idx)
                    ]
        (===) expect actual
    , testBytes
        "get 'abcd' 0 = 'a'"
        getBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 0
        ]
        (Test.Int.asOrPattern $ toInteger $ ord 'a')
    , testBytes
        "get 'abcd' 3 = 'd'"
        getBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 3
        ]
        (Test.Int.asOrPattern $ toInteger $ ord 'd')
    ]

test_substr :: [TestTree]
test_substr =
    [ testPropertyWithSolver "end < start -> substr bytes start end = ⊥" $ do
        str <- forAll genString
        delta <- forAll $ Gen.int (Range.linear 1 10)
        end <- forAll $ Gen.int (Range.linear 0 (T.length str - delta))
        let bytes = E.encode8Bit str
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    substrBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger $ end + delta)
                    , Test.Int.asInternal (toInteger end)
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b s e (e > length b). substr b s e = ⊥" $ do
        str <- forAll $ genString' 20
        end <- forAll $ Gen.int (Range.linear 21 30)
        let bytes = E.encode8Bit str
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    substrBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal 0
                    , Test.Int.asInternal (toInteger end)
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b s e (b < 0). substr b s e = ⊥" $ do
        str <- forAll genString
        begin <- forAll $ Gen.int (Range.linear (-256) (-1))
        end <- forAll $ Gen.int (Range.linear 0 256)
        let bytes = E.encode8Bit str
            expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    substrBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger begin)
                    , Test.Int.asInternal (toInteger end)
                    ]
        (===) expect actual
    , testSubstrBytes
        "substr 'abcd' 0 0 = ''"
        [ asInternal "abcd"
        , Test.Int.asInternal 0
        , Test.Int.asInternal 0
        ]
        (asOrPattern "")
    , testSubstrBytes
        "substr 'abcd' 0 1 = 'a'"
        [ asInternal "abcd"
        , Test.Int.asInternal 0
        , Test.Int.asInternal 1
        ]
        (asOrPattern "a")
    , testSubstrBytes
        "substr 'abcd' 1 3 = 'bc'"
        [ asInternal "abcd"
        , Test.Int.asInternal 1
        , Test.Int.asInternal 3
        ]
        (asOrPattern "bc")
    , testSubstrBytes
        "substr 'abcd' 0 4 = 'abcd'"
        [ asInternal "abcd"
        , Test.Int.asInternal 0
        , Test.Int.asInternal 4
        ]
        (asOrPattern "abcd")
    ]
  where
    testSubstrBytes ::
        HasCallStack =>
        TestName ->
        -- arguments of @substrBytes@ symbol
        [TermLike RewritingVariableName] ->
        -- expected result
        OrPattern RewritingVariableName ->
        TestTree
    testSubstrBytes testName = testBytes testName substrBytesSymbol

test_replaceAt :: [TestTree]
test_replaceAt =
    [ testPropertyWithSolver "∀ b i. replaceAt b i '' = n" $ do
        str <- forAll genString
        idx <- forAll $ Gen.int (Range.linear 0 256)
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    replaceAtBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger idx)
                    , asInternal ""
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b i (b /= ''). replaceAt '' i b = ⊥" $ do
        str <- forAll $ Gen.text (Range.linear 1 256) Gen.alphaNum
        idx <- forAll $ Gen.int (Range.linear 0 256)
        let expect = OrPattern.bottom
        actual <-
            evaluateTermT $
                mkApplySymbol
                    replaceAtBytesSymbol
                    [ asInternal ""
                    , Test.Int.asInternal (toInteger idx)
                    , asInternal $ E.encode8Bit str
                    ]
        (===) expect actual
    , testPropertyWithSolver
        "∀ b i b' (b' /= '', i >= length b). replaceAt b i b' = ⊥"
        $ do
            str <- forAll $ genString' 20
            idx <- forAll $ Gen.int (Range.linear 21 256)
            new <- forAll $ Gen.text (Range.linear 1 256) Gen.alphaNum
            let bytes = E.encode8Bit str
                bytes' = E.encode8Bit new
                expect = OrPattern.bottom
            actual <-
                evaluateTermT $
                    mkApplySymbol
                        replaceAtBytesSymbol
                        [ asInternal bytes
                        , Test.Int.asInternal (toInteger idx)
                        , asInternal bytes'
                        ]
            (===) expect actual
    , testBytes
        "replaceAt 'abcd' 0 '12' = '12cd'"
        replaceAtBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 0
        , asInternal "12"
        ]
        (asOrPattern "12cd")
    , testBytes
        "replaceAt 'abcd' 1 '12' = 'a12d'"
        replaceAtBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 1
        , asInternal "12"
        ]
        (asOrPattern "a12d")
    , testBytes
        "replaceAt 'abcd' 3 '12' = 'abc12'"
        replaceAtBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 3
        , asInternal "12"
        ]
        (asOrPattern "abc12")
    ]

test_padRight :: [TestTree]
test_padRight =
    [ testPropertyWithSolver "∀ b i v (i >= length b). padRight b i v = b" $ do
        str <- forAll genString
        val <- forAll Gen.alphaNum
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    padRightBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger $ BS.length bytes)
                    , Test.Int.asInternal (toInteger $ ord val)
                    ]
        (===) expect actual
    , testBytes
        "padRight 'abcd' 5 'e' = 'abcde"
        padRightBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 5
        , Test.Int.asInternal (toInteger $ ord 'e')
        ]
        (asOrPattern "abcde")
    ]

test_padLeft :: [TestTree]
test_padLeft =
    [ testPropertyWithSolver "∀ b i v (i >= length b). padLeft b i v = b" $ do
        str <- forAll genString
        val <- forAll Gen.alphaNum
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    padLeftBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal (toInteger $ BS.length bytes)
                    , Test.Int.asInternal (toInteger $ ord val)
                    ]
        (===) expect actual
    , testBytes
        "padLeft 'abcd' 5 'e' = 'eabcd"
        padLeftBytesSymbol
        [ asInternal "abcd"
        , Test.Int.asInternal 5
        , Test.Int.asInternal (toInteger $ ord 'e')
        ]
        (asOrPattern "eabcd")
    ]

test_reverse :: [TestTree]
test_reverse =
    [ testPropertyWithSolver "∀ b. reverse (reverse b) = b" $ do
        str <- forAll genString
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    reverseBytesSymbol
                    [ mkApplySymbol
                        reverseBytesSymbol
                        [ asInternal bytes
                        ]
                    ]
        (===) expect actual
    , testBytes
        "reverse 'abcd' = 'dcba'"
        reverseBytesSymbol
        [ asInternal "abcd"
        ]
        (asOrPattern "dcba")
    ]

test_length :: [TestTree]
test_length =
    [ testBytes
        "length 'abcd' = 4"
        lengthBytesSymbol
        [ asInternal "abcd"
        ]
        (Test.Int.asOrPattern 4)
    , testBytes
        "length '' = 0"
        lengthBytesSymbol
        [ asInternal ""
        ]
        (Test.Int.asOrPattern 0)
    ]

test_concat :: [TestTree]
test_concat =
    [ testPropertyWithSolver "∀ b. concat b '' = b" $ do
        str <- forAll genString
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    concatBytesSymbol
                    [ asInternal bytes
                    , asInternal ""
                    ]
        (===) expect actual
    , testPropertyWithSolver "∀ b. concat '' b = b" $ do
        str <- forAll genString
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    concatBytesSymbol
                    [ asInternal ""
                    , asInternal bytes
                    ]
        (===) expect actual
    , testBytes
        "concat 'abcd' 'efgh' = 'abcdefgh'"
        concatBytesSymbol
        [ asInternal "abcd"
        , asInternal "efgh"
        ]
        (asOrPattern "abcdefgh")
    ]

test_reverse_length :: TestTree
test_reverse_length =
    testPropertyWithSolver "∀ b. length (reverse b) = length b" $ do
        str <- forAll genString
        let bytes = E.encode8Bit str
            expect = Test.Int.asOrPattern $ toInteger $ BS.length bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    lengthBytesSymbol
                    [ mkApplySymbol
                        reverseBytesSymbol
                        [ asInternal bytes
                        ]
                    ]
        (===) expect actual

test_update_get :: TestTree
test_update_get =
    testPropertyWithSolver "∀ b i. update b i (get b i) = b" $ do
        str <- forAll $ Gen.text (Range.linear 1 256) Gen.alphaNum
        idx <- forAll $ Gen.int (Range.linear 0 (T.length str - 1))
        let bytes = E.encode8Bit str
            expect = asOrPattern bytes
        actual <-
            evaluateTermT $
                mkApplySymbol
                    updateBytesSymbol
                    [ asInternal bytes
                    , Test.Int.asInternal $ toInteger idx
                    , mkApplySymbol
                        getBytesSymbol
                        [ asInternal bytes
                        , Test.Int.asInternal $ toInteger idx
                        ]
                    ]
        (===) expect actual

test_bytes2string_string2bytes :: TestTree
test_bytes2string_string2bytes =
    testPropertyWithSolver "∀ s. bytes2string (string2bytes s) = s" $ do
        str <- forAll genString
        let expect = Test.String.asOrPattern str
        actual <-
            evaluateTermT $
                mkApplySymbol
                    bytes2stringBytesSymbol
                    [ mkApplySymbol
                        string2bytesBytesSymbol
                        [ Test.String.asInternal str
                        ]
                    ]
        (===) expect actual

test_decodeBytes_encodeBytes :: [TestTree]
test_decodeBytes_encodeBytes = map testProp encodings
  where
    testProp encoding =
        testPropertyWithSolver "∀ s. decodeBytes (encodeBytes s) = s" $ do
            str <- forAll genString
            let expect = Test.String.asOrPattern str
            actual <-
                evaluateTermT $
                    mkApplySymbol
                        decodeBytesBytesSymbol
                        [ Test.String.asInternal encoding
                        , mkApplySymbol
                            encodeBytesBytesSymbol
                            [ Test.String.asInternal encoding
                            , Test.String.asInternal str
                            ]
                        ]
            (===) expect actual
    encodings =
        [ "UTF-8"
        , "UTF-16LE"
        , "UTF-16BE"
        , "UTF-32LE"
        , "UTF-32BE"
        ]

test_decodeBytes :: TestTree
test_decodeBytes =
    testBadEvaluation
        "test bad decoding"
        decodeBytesKey
        ( mkApplySymbol
            decodeBytesBytesSymbol
            [ Test.String.asInternal "bad"
            , asInternal ""
            ]
        )

test_encodeBytes :: TestTree
test_encodeBytes =
    testBadEvaluation
        "test bad encoding"
        encodeBytesKey
        ( mkApplySymbol
            encodeBytesBytesSymbol
            [ Test.String.asInternal "bad"
            , Test.String.asInternal ""
            ]
        )

testBadEvaluation :: TestName -> Pretty.Doc a -> TermLike RewritingVariableName -> TestTree
testBadEvaluation testName hook term =
    testCase testName $ do
        try (runNoSMT $ evaluateTerm term) >>= \case
            Right patt ->
                assertFailure $
                    unlines
                        [ "Expected evaluation to fail, but it succeeded:"
                        , show patt
                        ]
            Left (ErrorCall errMsg) -> do
                let expectedErrMsg =
                        show $
                            Pretty.vsep
                                [ "Expecting hook " <> Pretty.squotes hook <> " to reduce concrete pattern:"
                                , Pretty.indent 4 (unparse term)
                                ]
                assertEqual "" expectedErrMsg errMsg

int2bytesData ::
    -- | (unsigned integer, signed integer, big endian?, bytes)
    [(Integer, Integer, Bool, ByteString)]
int2bytesData =
    [ (0, 0, True, "\x00\x00\x00\x00")
    , (128, -128, True, "\x80")
    , (2, 2, True, "\x02")
    , (254, -2, True, "\xfe")
    , (255, -1, True, "\xff")
    , (16, 16, True, "\x10")
    , (240, -16, True, "\xf0")
    , (128, 128, True, "\x00\x80")
    , (65408, -128, True, "\xff\x80")
    , (32768, -32768, True, "\x80\x00")
    , (128, 128, False, "\x80\x00")
    , (65408, -128, False, "\x80\xff")
    , (32768, -32768, False, "\x00\x80")
    , (0, 0, True, "")
    ]

test_int2bytes :: [TestTree]
test_int2bytes =
    map test int2bytesData
  where
    test ::
        HasCallStack =>
        (Integer, Integer, Bool, ByteString) ->
        TestTree
    test (integer, signed, bigEndian, bytes) =
        testCase name $ do
            let input =
                    int2bytes
                        (Test.Int.asInternal len)
                        (Test.Int.asInternal integer)
                        end
                expect = [asPattern bytes]
            actual <- simplify input
            assertEqual "" expect actual
            -- converting a signed integer should have the same result
            let signedInput =
                    int2bytes
                        (Test.Int.asInternal len)
                        (Test.Int.asInternal signed)
                        end
            signedActual <- simplify signedInput
            assertEqual "" expect signedActual
      where
        name =
            let args =
                    ( len
                    , integer
                    , if bigEndian then "BE" else "LE" :: String
                    )
             in show $ "int2bytes" <> Pretty.pretty args
        len = fromIntegral $ ByteString.length bytes
        end
            | bigEndian = bigEndianBytes
            | otherwise = littleEndianBytes

test_bytes2int :: [TestTree]
test_bytes2int =
    map test int2bytesData
  where
    test ::
        HasCallStack =>
        (Integer, Integer, Bool, ByteString) ->
        TestTree
    test (unsigned, signed, bigEndian, bytes) =
        testGroup name (mkCase <$> [True, False])
      where
        mkCase testSigned =
            testCase (if testSigned then "signed" else "unsigned") $ do
                let sign
                        | testSigned = signedBytes
                        | otherwise = unsignedBytes
                    input = bytes2int (asInternal bytes) end sign
                    int
                        | testSigned = signed
                        | otherwise = unsigned
                    expect =
                        [ Test.Int.asPattern int
                            & Pattern.mapVariables (pure mkConfigVariable)
                        ]
                actual <- simplify input
                assertEqual "" expect actual
        name =
            let args =
                    ( ByteString.unpack bytes
                    , if bigEndian then "BE" else "LE" :: String
                    , "_" :: String
                    )
             in show $ "bytes2int" <> Pretty.pretty args
        end
            | bigEndian = bigEndianBytes
            | otherwise = littleEndianBytes

test_InternalBytes :: [TestTree]
test_InternalBytes =
    [ testCase "\\dv{Bytes{}}(\"00\")" $ do
        let unverified =
                mkDomainValue $
                    DomainValue bytesSort $
                        mkStringLiteral "00"
            expect = Right $ asInternal "00"
            actual = verifyPattern (Just bytesSort) unverified
        assertEqual "" expect actual
    , testCase "\\dv{Bytes{}}(\"\\x00\")" $ do
        let unverified =
                mkDomainValue $
                    DomainValue bytesSort $
                        mkStringLiteral "\x00"
            expect = Right $ asInternal "\x00"
            actual = verifyPattern (Just bytesSort) unverified
        assertEqual "" expect actual
    ]

test_unparse :: [TestTree]
test_unparse =
    [ testCase "unparse using 8-bit encoding" $ do
        let input = asInternal "\x00" :: TermLike RewritingVariableName
            actual = (show . unparse) input
            expect = "\\dv{Bytes{}}(\"\\x00\")"
        assertEqual "" expect actual
    ]

-- * Helpers

asInternal :: InternalVariable variable => ByteString -> TermLike variable
asInternal = InternalBytes.asInternal bytesSort

asPattern :: InternalVariable variable => ByteString -> Pattern variable
asPattern = InternalBytes.asPattern bytesSort

asOrPattern :: InternalVariable variable => ByteString -> OrPattern variable
asOrPattern = MultiOr.singleton . asPattern

testBytes ::
    HasCallStack =>
    String ->
    Symbol ->
    [TermLike RewritingVariableName] ->
    OrPattern RewritingVariableName ->
    TestTree
testBytes name = testSymbolWithoutSolver evaluateTerm name
